open Graphics
open Format
open Lowlevelgraph.TwoDRoutines
open Lowlevelgraph.AntEnv 
open Utils.Pervasive
open Utils.Error
open Syntax
open Pointers
open Core
open PrintExpr
open Binding
open GPUtils 
open GtkText


let error_log str =
		let file_name =  "errors.txt" in 
		let file_channel = open_out_gen 
			[Open_creat; Open_append; Open_creat] 
			666 file_name in
		
		output_string file_channel str;
		flush file_channel;
		close_out file_channel
let make_win_title expr = 
	match expr with
	| Ty (_, None) -> "An unamed type:"
	| Ty (_, Some name) -> "A name (\"" ^ name ^ "\") for the type:"
	| Te (te, None)-> "An unamed term:" 
	| Te (te, Some name) -> "A name (\"" ^ name ^ "\") for the term:" 
		
let view_fvar_routine ctx expr ( ) = ( )(*
	let window = GWindow.window 
		~border_width:10 
		~title:"free vars" () in
		un (window #connect#destroy ~callback:window#destroy);
		let box1 = GPack.vbox ~packing:window#add () in
	
		let vars = GBin.frame ~label:"Vars..." ~packing:box1#pack () in
		let text = match expr with
		|Ty _ -> "Expression is a type"
		|Te (te, _) -> 
			String.concat "\n" 
			(List.map (fun te -> string_of_term ctx te Alpha) (free_term_vars ctx te))
		in
		un(GMisc.label
		~text:text ~packing:vars#add ( ));	
	window#show( )	*)




type expression_argument = ExpressionString of string | RawExpression of t_Expr		
let rec make_expr_panel env expr_str ctx = 	
	let panel title = 
		let pan = GBin.frame ~label:(title^ "...") ~packing:env#add ( ) in
		GPack.vbox ~width:580 ~packing:pan#add ( ) in
	
	let evalPanel = panel "Expression" in
		let box_eval = GPack.hbox ~packing:evalPanel#add () in
		let box_eval_left = GPack.vbox ~packing:box_eval#add () in
		let expr_label = GText.view 
			~width:300 
			~height:300 
			~border_width:3 
			~wrap_mode:`WORD
			~packing:box_eval_left#add( ) 	in 
	
	expr_label#buffer#set_text expr_str;
		
		
	let unevaluated_expression ( ) = parse_string (expr_label#buffer#get_text( )) ctx in
	let evaluated_expression ( ) = 
			match unevaluated_expression ( ) with
			| Ty (ty , _) -> Ty (ty, None)
			| Te (te, _) -> Te (normalize ctx te, None) in

	let box_eval_right = GPack.vbox ~packing:box_eval#add () in
	let eval_button = GButton.button ~label:"eval" 
		~packing:box_eval_right#pack () in	
	let visual_btn = GButton.check_button  ~label:"Visual" ~packing:box_eval_right#add () in

	
	let eval_routine ( ) =
		let new_expr =  evaluated_expression ( ) in 
		match new_expr with 
		| Te (te, _) -> 
			begin match typeof ctx te with
			| TyUnit -> 
				let tick = ref 200 in 
				let timer ( ) = 
					tick := !tick -1; 
					if !tick > 0 then true else false in
					un(playAnt ~visual:visual_btn#active timer 60. ctx te)
			|_-> show_expr_window ctx (RawExpression new_expr) ( )
			end
		|_->show_expr_window ctx (RawExpression new_expr) ( ) in
	
	
	
	un (eval_button#connect#clicked ~callback:eval_routine);
	match (unevaluated_expression ( ))  with
	| Te (te, _) -> 
		let box_typeof = GPack.hbox ~packing:evalPanel#add () in
		let ty = typeof ctx te in
		let box_typeof_left = GPack.vbox ~packing:box_typeof#add () in
		let type_label = GEdit.entry 
		~editable:false
		~text:"" 
		~width:500 
		~packing:box_typeof_left#add () in
		type_label#set_text ("Of type: " ^ (string_of_type ctx ty Alpha));
		
		let box_typeof_right = GPack.vbox ~packing:box_typeof#add () in
		let view_type = GButton.button ~label:"Open" 
		~packing:box_typeof_right#pack () in
		un (view_type#connect#clicked 
			~callback:(show_expr_window ctx (RawExpression(Ty (ty, None))) ))		
	|_->()
	

and show_expr_window ctx expr_arg ( ) = 
	
	let str  = match expr_arg with
		| RawExpression expr -> "(" ^ (string_of_expr ctx expr Compact) ^ ")"
		| ExpressionString str -> str in
		
	let expr = match expr_arg with
		| RawExpression expr -> expr
		| ExpressionString str -> parse_string str ctx in
		
	let title = make_win_title expr in
	let window = GWindow.window 
		~border_width:10 
		~title:title () in
		un (window #connect#destroy ~callback:window#destroy);
		(*un(close_button#connect#clicked ~callback:window#destroy);*)
	
	let hBox = GPack.hbox ~packing:window#add () in
	let boxMenu = GPack.vbox  ~packing:hBox#add () in
	
	make_expr_panel boxMenu str  ctx;
	window#show( )
	
	
	
	
	
	
	
	